package dbc;

import java.io.IOException;
import java.io.PrintWriter;
import java.util.Set;
import javax.annotation.processing.AbstractProcessor;
import javax.annotation.processing.Filer;
import javax.annotation.processing.RoundEnvironment;
import javax.annotation.processing.SupportedAnnotationTypes;
import javax.annotation.processing.SupportedSourceVersion;
import javax.lang.model.SourceVersion;
import javax.lang.model.element.Element;
import javax.lang.model.element.ExecutableElement;
import javax.lang.model.element.Modifier;
import javax.lang.model.element.TypeElement;
import javax.lang.model.element.VariableElement;
import javax.lang.model.type.TypeMirror;
import javax.lang.model.util.Types;
import javax.tools.Diagnostic.Kind;
import javax.tools.StandardLocation;

/**
* PreProcessor is called at compilation time to process
* all @Pre annotations in the source code.
* For each method annoted with @Pre, this processor will create
* an aspect per method which will have to be compile with aspectj.
*/
// PreProcessor supports only @Pre annotations
@SupportedAnnotationTypes({"dbc.Pre"})
// Only Java >= 6 is supported
@SupportedSourceVersion(SourceVersion.RELEASE_6)
public class PreProcessor extends AbstractProcessor {
    /**
     * Process is called during compilation to parse all @Invariant annotations
     * @param annotations A set containing all @Invariant annotations
     * @param roundEnv Object representating the current step of annotations processing
     * @return true on success
     */
    @Override
    public boolean process(Set<? extends TypeElement> annotations, RoundEnvironment roundEnv) {
	// Creating ressources for output resulting file
        Filer filer = processingEnv.getFiler();
        Types types = processingEnv.getTypeUtils();
	
	// Get all Elements (here methods) annoted with @Pre
	// Each Element will be process to create an aspect
        for(Element element : roundEnv.getElementsAnnotatedWith(Pre.class)) {
            try {
		// Getting usefull informations such as class name to generate an unique aspect name
                TypeMirror classType = element.getEnclosingElement().asType();

                String className = classType.toString();
                String erasedClassName = types.erasure(classType).toString();

                String methodName = element.getSimpleName().toString();
                
                String aspectName = "PreAspect_" + erasedClassName + "_" + methodName;
                aspectName = aspectName.replace(".", "_");

                PrintWriter pw = new PrintWriter(
                        filer.createResource(StandardLocation.SOURCE_OUTPUT,
                                             "aspects", aspectName + ".aj")
                                             .openOutputStream());
		
		// Here we have the pre annotation
                Pre pre = element.getAnnotation(Pre.class);
		// Analyze pre annotation to handle special operators such as $forall
                SyntaxHandler sh = new SyntaxHandler(pre.value());
                sh.processExpression();
                String condition = sh.getProcessedExpression();

                boolean isStatic = element.getModifiers().contains(Modifier.STATIC);

                ExecutableElement exec = (ExecutableElement) element;

                String paramNames = "";
                String paramList = "";
                String erasedParamTypes = "";
                String erasedParamList = "";
                for(VariableElement param : exec.getParameters()) {
                    TypeMirror type = param.asType();
                    String name = param.getSimpleName().toString();

                    if(!paramList.isEmpty()) {
                        paramNames += ", ";
                        paramList += ", ";
                        erasedParamTypes += ", ";
                        erasedParamList += ", ";
                    }

                    paramNames += name;
                    paramList += type + " " + name;
                    erasedParamTypes += types.erasure(type);
                    erasedParamList += types.erasure(type) + " " + name;
                }

                //Aspect generation
                pw.println("privileged aspect " + aspectName + " implements dbc.Contract {");

                pw.print("private ");
                if(isStatic) pw.print("static ");
                pw.println("void " + erasedClassName + ".preAssert"+methodName+"(" + erasedParamList + ") {");
                pw.println(sh.getGeneratedCode());
//                pw.println("System.out.println(\"Precondition " + pre.value().replace("\"", "\\\"") + " \" + (" + condition + "));");
                pw.println("if(!(" + condition + ")) {");
                pw.print("throw new dbc.PreConditionException(\"Precondition violated in ");
                pw.println(className + "." + methodName + "(" + paramList + ")\");");
                pw.println("}");
                pw.println("}");

                pw.print("before(" + erasedParamList + "): ");
                pw.print("call(* " + erasedClassName + "." + methodName + "(" + erasedParamTypes + "))");
                pw.println(" && args(" + paramNames + ") && !within(dbc.Contract+) {");
                if(isStatic) {
                    pw.print(erasedClassName);
                } else {
                    pw.print("((" + erasedClassName + ")thisJoinPoint.getTarget())");
                }
                pw.println(".preAssert"+methodName+"(" + paramNames + ");");
                pw.println("}}");

                pw.close();

                
            } catch(IOException ex) {
		// If something goes wrong display a warning and return
                processingEnv.getMessager().printMessage(Kind.WARNING, ex.getMessage());
            }
        }

        return true;
    }
}
